Introduction to Formal Methods (2018)
Staff
- Hossein Hojjat (office 2-615) hojjat at sign ut dot ac dot ir
- Fetemeh Ghassemi (office 2-611) fghassemi at sign ut dot ac dot ir
- Ramtin Khosravi (office 2-508) r.khosravi at sign ut dot ac dot ir
Schedule
| Week 1 | ||
|---|---|---|
| Sunday 1 Mehr (Sep. 23) | Lecture 1: Course Overview | slides |
| Tuesday 3 Mehr (Sep. 25) | Lecture 2: Boolean Satisfiability (SAT) Solving | slides |
| Week 2 | ||
| Sunday 8 Mehr (Sep. 30) | Lecture 3: Bounded Model Checking | slides |
| Tuesday 10 Mehr (Oct. 2) | Lecture 4: Satisfiability Modulo Theories | slides |
| Week 3 | ||
| Sunday 15 Mehr (Oct. 7) | Lecture 5: From Programs to Formulas | slides |
| Tuesday 17 Mehr (Oct. 9) | Lecture 6: Hoare Logic | slides |
| Week 4 | ||
| Sunday 22 Mehr (Oct. 14) | Lecture 7: Hoare Logic Rules | slides |
| Tuesday 24 Mehr (Oct. 16) | Lecture 8: Propagating Preconditions and Postconditions | slides |
| Week 5 | ||
| Sunday 29 Mehr (Oct. 21) | Lecture 9: Verification by Solving Horn Clauses | slides |
| Tuesday 1 Aban (Oct. 23) | Lecture 10: Verifying Programs with Arrays & Dynamic Allocation | slides |
| Week 6 | ||
| Sunday 6 Aban (Oct. 28) | Lecture 11: Hoare Logic for Concurrent Programs | slides |
| Tuesday 8 Aban (Oct. 30) | No class | |
| Week 7 | ||
| Sunday 13 Aban (Nov. 4) | Lecture 12: Symbolic and Concolic Execution | slides |
| Tuesday 15 Aban (Nov. 6) | Lecture 13: Introduction to Model Checking | slides |
| Week 8 | ||
| Sunday 20 Aban (Nov. 11) | Lecture 14: Modeling Hardware/Software Systems | slides |
| Tuesday 22 Aban (Nov. 13) | Lecture 15: Modeling Parallel and Communicating Systems (Part 1) | slides |
| Week 9 | ||
| Sunday 27 Aban (Nov. 17) | Lecture 16: Modeling Parallel and Communicating Systems (Part 2) | slides |
| Tuesday 29 Aban (Nov. 19) | Lecture 17: Modeling Checking with Spin | slides |
| Week 10 | ||
| Sunday 4 Azar (Nov. 25) | No class | |
| Tuesday 6 Azar (Nov. 27) | Lecture 18: Linear Time Properties | slides |
| Week 11 | ||
| Sunday 11 Azar (Dec. 2) | Lecture 19: Safety Properties | slides |
| Tuesday 13 Azar (Dec. 4) | Lecture 20: Liveness Properties and Fairness | slides |
| Week 12 | ||
| Sunday 18 Azar (Dec. 9) | Lecture 21: Regular Safety Properties | slides (on CECM) |
| Tuesday 20 Azar (Dec. 11) | Lecture 22: Model Checking ω-Regular Properties | slides (1) slides (2) (on CECM) |
| Week 13 | ||
| Sunday 25 Azar (Dec. 16) | Lecture 23: Linear Temporal Logic (LTL) | slides (1) slides (2) (on CECM) |
| Tuesday 27 Azar (Dec. 18) | Lecture 24: Modeling and Analysis using Rebeca | slides |
| Week 14 | ||
| Sunday 2 Dey (Dec. 23) | Lecture 25: The Palang Language | handouts |
| Tuesday 4 Dey (Dec. 25) | Lecture 26: Software Model Checking | slides |
| Week 15 | ||
| Sunday 9 Dey (Dec. 30) | Lecture 27: | |
| Tuesday 11 Dey (Jan. 1) | Lecture 28: Introduction to Model-Based Testing | slides |
Assignments
- SAT Solver - due date Mehr 13th (October 5)
- Automatic Program Verifier - due date Aban 11th (November 2)
- Concolic Execution (bestteam.exe) - due date Aban 30th (November 21)
- Spin Modeling - due date Azar 30th (Dec. 21)
Homework
- HW 1 - due date Azar 25th (Dec. 16)
- HW 2 - Solve problems 4.6, 4.12, 4.19, 5.2, and 5.13 of PMC - due date Dey 9 (Dec. 30)